'''
Created on 18/05/2011

@author: Jose Rodriguez Shaw, Sebastian Caredio, Agustin Ventura
'''     

import arbol
import translator 
    
'''
1. Si el arbol es nulo, no hay reduccion
2. Saco la raiz del arbol actual
3. Si la raiz es @:
3.1. Llamo a redex en el hijo izq.
3.1.1. Si tengo una variable cuyo numero es igual al max de lambdas hasta el momento
3.1.1.1. Aumento en uno mas de la cantidad de lambdas hasta el momento a 
todas las variables libres en la aplicacion a sustituir
3.1.1.2. Sustituyo con el arbol obtenido en el punto 3.1.1.1.
3.1.2. Si tengo una variable cuyo numero es menor al max de lambdas hasta el momento
3.1.2.1. Reduzco en uno el valor de la variable.
3.2. Si no es @ sigo recorriendo para ambas ramas

Este metodo devuelve un arbol reducido que deberia ser igual al valor de verdad de
la expresin booleana original
'''    
def reductTree(arbolDeBruijn):
    if (arbolDeBruijn.esVacio()):
        return arbol.TArbol()
    else:
        raiz = arbolDeBruijn.obtenerRaiz()
        resultado = arbol.TArbol()
        resultado.insertar(reductor(raiz))
        return resultado

'''
Esta es la funcion recursiva que efectivamente hace las reducciones
Devuelve un elemento de arbol ya reducido
'''
def reductor(deBruijnElem):
    #llamo recursivamente en busca de aplicaciones
    
    while (not(deBruijnElem.estaVisitado()) and(deBruijnElem.hijoIzq <> None or deBruijnElem.hijoDer <> None) and deBruijnElem.datos <> '@'):
        deBruijnElem.visitar() 
        if (deBruijnElem.hijoIzq <> None):
            deBruijnElem.hijoIzq = reductor(deBruijnElem.hijoIzq)
        if (deBruijnElem.hijoDer <> None):
            deBruijnElem.hijoDer = reductor(deBruijnElem.hijoDer)
    #si encuentro una aplicacion entonces realizo reducciones
    if (deBruijnElem.datos == '@'):
        #me quedo con la aplicacion a la derecha que sera lo que se susituira
        #el varRedex sera lo que esta a la izquierda pero tambien luego de aplicar las
        #reducciones que sean necesarias
        varRedex = reductor(deBruijnElem.hijoDer)
        #una vez encontrada la aplicacion, busco el primer lambda en el hijo izquierdo
        varLambda = deBruijnElem.hijoIzq
        while (varLambda <>None and(varLambda.hijoDer <> None or varLambda.hijoIzq <> None) and varLambda.datos <> 'l'):
            #si no esta en el primer lambda a la izquierda, deberia estar a la derecha en los
            #sucesivos pasos o si se encuentra una aplicacin, denuevo a la izquierda de esta
            if (varLambda.datos == '@'):
                if (varLambda.hijoDer <> None):
                    varLambda = varLambda.hijoDer #--? no debria ser izq
            else:
                if (varLambda.hijoIzq <> None):
                    varLambda = varLambda.hijoIzq
        #si varLambda es diferente a l quiere decir que no encontre lambdas
        #en el caso de que no  haya lambdas, entonces no hago nada, por eso el if
        #agregue varLambda <>None por que daba error por que valLambda es null no se puede preguntar por datos
        if (varLambda <> None and varLambda.datos == 'l'):
            #una vez encontrado el lambda, llamo a la funcion redex sobre el resto
            #le paso 1 a la funcion pq recien encontre un lambda
            newVarLambda = redex(varLambda.hijoDer, varRedex, 1)
            #una vez hechas todas las reducciones quito la aplicacion y saco el lambda reducido
            deBruijnElem.hijoDer = None
            deBruijnElem.hijoIzq = newVarLambda
           
    return deBruijnElem

def redex(varLambda, varRedex, maxLambda):
    #si el elemento actual es diferente de l o @, entonces es un numero, lo comparo con
    #maxLambda y si son iguales, entonces lo sustituyo con la aplicacion
    if (varLambda == None):
        return None
    elif (varLambda.datos <> '@' and varLambda.datos <> 'l'):
        if (varLambda.datos == maxLambda):
            #si sustituyo, entonces aumento la numeracion segun la cantidad de lambdas que 
            #tengo hasta el momento con la funcion incrementarLibres()
            varRedex = incrementarLibres(varRedex, maxLambda)
            varLambda = varRedex
        return varLambda
    #si es @, sigo llamando recursivamente sin aumentar la cantidad de lambdas
    elif (varLambda.datos == '@'):
        if (varLambda.hijoIzq <> None):
            varLambda.hijoIzq = redex(varLambda.hijoIzq, varRedex, maxLambda)
        if (varLambda.hijoDer <> None):
            varLambda.hijoDer = redex(varLambda.hijoDer, varRedex, maxLambda)
        return varLambda
    #si es l, entonces llamo recursivamente aumentando en una maxlambda
    elif (varLambda.datos == 'l'):
        if (varLambda.hijoIzq <> None):
            varLambda.hijoIzq = redex(varLambda.hijoIzq, varRedex, maxLambda + 1)
        if (varLambda.hijoDer <> None):
            varLambda.hijoDer = redex(varLambda.hijoDer, varRedex, maxLambda + 1)
        return varLambda
    
def incrementarLibres(varRedex, maxLambda):
    if (varRedex.datos <> 'l' and varRedex.datos <> '@'):
        varRedex.datos = maxLambda
        if (varRedex.hijoDer <> None):
            varRedex.hijoDer = incrementarLibres(varRedex.hijoDer, maxLambda + 1)
            if (varRedex.hijoIzq <> None):
                varRedex.hijoIzq = incrementarLibres(varRedex.hijoIzq, maxLambda + 2)
        elif (varRedex.hijoIzq <> None):
            varRedex.hijoIzq = incrementarLibres(varRedex.hijoIzq, maxLambda + 1)
    #si es l o @, llamo recursivamente pero sin aumentar maxLambda
    else:
        if (varRedex.hijoDer <> None):
            varRedex.hijoDer = incrementarLibres(varRedex.hijoDer, maxLambda)
        if (varRedex.hijoIzq <> None):
            varRedex.hijoIzq = incrementarLibres(varRedex.hijoIzq, maxLambda)
    return varRedex
'''
Este metodo devuelve un True o False, dependiendo si la recorrida inOrden del arbol reducido
es igual a la recorrida in orden del valor de verdad pasado por parametro
'''
def verify(truthValue, reducedTree):
    stringTree = reducedTree.inOrden()
    treeTruthValue = arbol.TArbol()
    if (truthValue == True):
        treeTruthValue.insertar(translator.genElemTrue())
    else:
        treeTruthValue.insertar(translator.genElemFalse())
    stringTruthValue = treeTruthValue.inOrden()
    return (stringTree == stringTruthValue)